package scala.examples.tcpoly.calculi.lambda.full

// See Emir et al. "Matching objects with patterns"
// using extractors to encapsulate the change of Abs(x: Name, t: Term) to Abs(a: \\[Term])
// pattern matching on Abs automatically generates a fresh binder for the abstraction so as to avoid capture
trait Syntax { self: Syntax with Binding  =>
  trait Term extends Nominal[Term]{
    def isValue: Boolean
  }

  case class Var(name: Name) extends Term {
    def isValue = false

    def swap(a: Name, b: Name) = Var(name swap(a, b))
    def fresh(a: Name) = name fresh(a)
  }

  object Abs {
    def apply(x: Name, body: Term) = new Abs(\\(x, body))
    def apply(abs: \\[Term]) = new Abs(abs)
    def unapply(a: Abs): Some[(Name, Term)] = \\.unapply(a.abs)
  }
  class Abs(val abs: \\[Term]) extends Term {
    def isValue = true

    def swap(a: Name, b: Name) =  Abs(abs swap(a, b))
    def fresh(a: Name) = abs fresh(a)
  }

  case class App(fun: Term, arg: Term) extends Term {
    def isValue = false

    def swap(a: Name, b: Name) = App(fun swap(a, b), arg  swap(a, b))
    def fresh(a: Name) = fun.fresh(a) && arg.fresh(a)
  }

  class Literal extends Term { 
    def isValue = true 
    def swap(a: Name, b: Name) = this
    def fresh(a: Name) = true    
  }
  case object t extends Literal
  case object f extends Literal
}

